|
| creator |
König, Barbara
| | Kozioura, Vitali
| | date |
2006-02-02
| | | | description |
25 pages
| |
Graph transformation systems are a general specification language
for systems with dynamically changing topologies, such as mobile and
distributed systems. Although in the last few years several analysis
and verification methods have been proposed for graph transformation
systems, counterexample-guided abstraction refinement has not yet
been studied in this setting.
We propose a counterexample-guided abstraction refinement technique
which is based on the over-approximation of graph transformation
systems by Petri nets. We show that a spurious counterexample is
caused by merging nodes during the approximation. We present a
technique for identifying these merged nodes and splitting them
using abstraction refinement, which removes the spurious run. The
technique has been implemented in the Augur tool and experimental
results are discussed.
| | format |
application/pdf
| | 289110 Bytes | |